n, m:. firstn(n;upto(m)) ~ if nm upto(n) else upto(m) fi 

latex

Definitions	S  T, Top, ||as||, {i..j}, A, False, i  j < k, as @ bs, map(f;as), upto(n), Unit, P  Q, P & Q, P  Q, T, P  Q, ij, , AB, , i<j, b, b, x:A. B(x), True, t  T, Prop
Lemmas	bnot wf, assert wf, lt int wf, le wf, bool wf, le int wf, assert of lt int, bnot of le int, true wf, squash wf, eqff to assert, iff transitivity, assert of le int, eqtt to assert, nat wf, upto decomp, upto wf, int seg wf, top wf, map wf, firstn append, length upto, firstn all